Theorem vtoclbg 3523

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 348	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3521	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-clel 2839

This theorem is used by:  alexeqg  3608  pm13.183  3623  elab6g  3626  elabgw  3634  sbc8g  3750  sbc2or  3751  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcie2g  3782  eqsbc1  3788  sbcng  3789  sbcimg  3790  sbcan  3791  sbcor  3792  sbcbig  3793  sbcal  3801  sbcex2  3802  sbcel1v  3807  sbcreu  3827  csbiebg  3883  sbcel12  4372  sbceqg  4373  csbie2df  4404  preq12bg  4813  elintrabg  4926  sbcbr123  5166  inisegn0  6114  fsn2g  7171  funfvima3  7273  elixpsn  9003  ixpsnf1o  9004  domeng  9027  elhf2g  9948  rankcf  10901  kardeng  35966  eldm3  36741  elima4  36755  brsset  36866  brbigcup  36875  elfix2  36881  elfunsg  36893  elsingles  36895  funpartlem  36921  ellines  37132  bj-elpwgALT  38239  cover2g  38918