Theorem vtoclbg 3512

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 345	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3509	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  alexeqg  3606  pm13.183  3621  elab6g  3624  elabgw  3633  sbc8g  3750  sbc2or  3751  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcie2g  3783  eqsbc1  3789  sbcng  3790  sbcimg  3791  sbcan  3792  sbcor  3793  sbcbig  3794  sbcal  3802  sbcex2  3803  sbcel1v  3808  sbcreu  3828  csbiebg  3883  sbcel12  4362  sbceqg  4363  csbie2df  4394  preq12bg  4804  elintrabg  4911  sbcbr123  5146  inisegn0  6049  fsn2g  7072  funfvima3  7172  elixpsn  8864  ixpsnf1o  8865  domeng  8888  rankcf  10671  eldm3  35738  elima4  35753  brsset  35867  brbigcup  35876  elfix2  35882  elfunsg  35894  elsingles  35896  funpartlem  35920  ellines  36130  elhf2g  36154  bj-elpwgALT  37032  cover2g  37700  sbcrexgOLD  42762